Left Termination proof of /tmp/tmp7W5

Left Termination of the query pattern f(b,f,f) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

f₃(0₀, Y, 0₀).
f₃(s₁(X), Y, Z) :- f₃(X, Y, U), f₃(U, Y, Z).

With regard to the inferred argument filtering the predicates were used in the following modes:
f₃: (b,f,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

f_3_in_gaa₃(0_0, Y, 0_0) -> f_3_out_gaa₃(0_0, Y, 0_0)
f_3_in_gaa₃(s_1₁(X), Y, Z) -> if_f_3_in_1_gaa₄(X, Y, Z, f_3_in_gaa₃(X, Y, U))
if_f_3_in_1_gaa₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_in_gaa₃(U, Y, Z))
if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_out_gaa₃(U, Y, Z)) -> f_3_out_gaa₃(s_1₁(X), Y, Z)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

f_3_in_gaa₃(0_0, Y, 0_0) -> f_3_out_gaa₃(0_0, Y, 0_0)
f_3_in_gaa₃(s_1₁(X), Y, Z) -> if_f_3_in_1_gaa₄(X, Y, Z, f_3_in_gaa₃(X, Y, U))
if_f_3_in_1_gaa₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_in_gaa₃(U, Y, Z))
if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_out_gaa₃(U, Y, Z)) -> f_3_out_gaa₃(s_1₁(X), Y, Z)

F_3_IN_GAA₃(s_1₁(X), Y, Z) -> IF_F_3_IN_1_GAA₄(X, Y, Z, f_3_in_gaa₃(X, Y, U))
F_3_IN_GAA₃(s_1₁(X), Y, Z) -> F_3_IN_GAA₃(X, Y, U)
IF_F_3_IN_1_GAA₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> IF_F_3_IN_2_GAA₅(X, Y, Z, U, f_3_in_gaa₃(U, Y, Z))
IF_F_3_IN_1_GAA₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> F_3_IN_GAA₃(U, Y, Z)

The TRS R consists of the following rules:

f_3_in_gaa₃(0_0, Y, 0_0) -> f_3_out_gaa₃(0_0, Y, 0_0)
f_3_in_gaa₃(s_1₁(X), Y, Z) -> if_f_3_in_1_gaa₄(X, Y, Z, f_3_in_gaa₃(X, Y, U))
if_f_3_in_1_gaa₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_in_gaa₃(U, Y, Z))
if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_out_gaa₃(U, Y, Z)) -> f_3_out_gaa₃(s_1₁(X), Y, Z)

The argument filtering Pi contains the following mapping:
f_3_in_gaa₃(x1, x2, x3) = f_3_in_gaa₁(x1)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
f_3_out_gaa₃(x1, x2, x3) = f_3_out_gaa₁(x3)
if_f_3_in_1_gaa₄(x1, x2, x3, x4) = if_f_3_in_1_gaa₁(x4)
if_f_3_in_2_gaa₅(x1, x2, x3, x4, x5) = if_f_3_in_2_gaa₁(x5)
IF_F_3_IN_2_GAA₅(x1, x2, x3, x4, x5) = IF_F_3_IN_2_GAA₁(x5)
IF_F_3_IN_1_GAA₄(x1, x2, x3, x4) = IF_F_3_IN_1_GAA₁(x4)
F_3_IN_GAA₃(x1, x2, x3) = F_3_IN_GAA₁(x1)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

F_3_IN_GAA₃(s_1₁(X), Y, Z) -> IF_F_3_IN_1_GAA₄(X, Y, Z, f_3_in_gaa₃(X, Y, U))
F_3_IN_GAA₃(s_1₁(X), Y, Z) -> F_3_IN_GAA₃(X, Y, U)
IF_F_3_IN_1_GAA₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> IF_F_3_IN_2_GAA₅(X, Y, Z, U, f_3_in_gaa₃(U, Y, Z))
IF_F_3_IN_1_GAA₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> F_3_IN_GAA₃(U, Y, Z)

The TRS R consists of the following rules:

f_3_in_gaa₃(0_0, Y, 0_0) -> f_3_out_gaa₃(0_0, Y, 0_0)
f_3_in_gaa₃(s_1₁(X), Y, Z) -> if_f_3_in_1_gaa₄(X, Y, Z, f_3_in_gaa₃(X, Y, U))
if_f_3_in_1_gaa₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_in_gaa₃(U, Y, Z))
if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_out_gaa₃(U, Y, Z)) -> f_3_out_gaa₃(s_1₁(X), Y, Z)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

IF_F_3_IN_1_GAA₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> F_3_IN_GAA₃(U, Y, Z)
F_3_IN_GAA₃(s_1₁(X), Y, Z) -> F_3_IN_GAA₃(X, Y, U)
F_3_IN_GAA₃(s_1₁(X), Y, Z) -> IF_F_3_IN_1_GAA₄(X, Y, Z, f_3_in_gaa₃(X, Y, U))

The TRS R consists of the following rules:

f_3_in_gaa₃(0_0, Y, 0_0) -> f_3_out_gaa₃(0_0, Y, 0_0)
f_3_in_gaa₃(s_1₁(X), Y, Z) -> if_f_3_in_1_gaa₄(X, Y, Z, f_3_in_gaa₃(X, Y, U))
if_f_3_in_1_gaa₄(X, Y, Z, f_3_out_gaa₃(X, Y, U)) -> if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_in_gaa₃(U, Y, Z))
if_f_3_in_2_gaa₅(X, Y, Z, U, f_3_out_gaa₃(U, Y, Z)) -> f_3_out_gaa₃(s_1₁(X), Y, Z)

The argument filtering Pi contains the following mapping:
f_3_in_gaa₃(x1, x2, x3) = f_3_in_gaa₁(x1)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
f_3_out_gaa₃(x1, x2, x3) = f_3_out_gaa₁(x3)
if_f_3_in_1_gaa₄(x1, x2, x3, x4) = if_f_3_in_1_gaa₁(x4)
if_f_3_in_2_gaa₅(x1, x2, x3, x4, x5) = if_f_3_in_2_gaa₁(x5)
IF_F_3_IN_1_GAA₄(x1, x2, x3, x4) = IF_F_3_IN_1_GAA₁(x4)
F_3_IN_GAA₃(x1, x2, x3) = F_3_IN_GAA₁(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ RuleRemovalProof

Q DP problem:
The TRS P consists of the following rules:

IF_F_3_IN_1_GAA₁(f_3_out_gaa₁(U)) -> F_3_IN_GAA₁(U)
F_3_IN_GAA₁(s_1₁(X)) -> F_3_IN_GAA₁(X)
F_3_IN_GAA₁(s_1₁(X)) -> IF_F_3_IN_1_GAA₁(f_3_in_gaa₁(X))

The TRS R consists of the following rules:

f_3_in_gaa₁(0_0) -> f_3_out_gaa₁(0_0)
f_3_in_gaa₁(s_1₁(X)) -> if_f_3_in_1_gaa₁(f_3_in_gaa₁(X))
if_f_3_in_1_gaa₁(f_3_out_gaa₁(U)) -> if_f_3_in_2_gaa₁(f_3_in_gaa₁(U))
if_f_3_in_2_gaa₁(f_3_out_gaa₁(Z)) -> f_3_out_gaa₁(Z)

The set Q consists of the following terms:

f_3_in_gaa₁(x0)
if_f_3_in_1_gaa₁(x0)
if_f_3_in_2_gaa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {F_3_IN_GAA₁, IF_F_3_IN_1_GAA₁}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

IF_F_3_IN_1_GAA₁(f_3_out_gaa₁(U)) -> F_3_IN_GAA₁(U)

Strictly oriented rules of the TRS R:

f_3_in_gaa₁(0_0) -> f_3_out_gaa₁(0_0)
if_f_3_in_1_gaa₁(f_3_out_gaa₁(U)) -> if_f_3_in_2_gaa₁(f_3_in_gaa₁(U))

Used ordering: POLO with Polynomial interpretation:

POL(0_0) = 2
POL(if_f_3_in_1_gaa₁(x₁)) = 2·x₁
POL(f_3_out_gaa₁(x₁)) = 1 + x₁
POL(F_3_IN_GAA₁(x₁)) = x₁
POL(s_1₁(x₁)) = 2·x₁
POL(IF_F_3_IN_1_GAA₁(x₁)) = x₁
POL(f_3_in_gaa₁(x₁)) = 2·x₁
POL(if_f_3_in_2_gaa₁(x₁)) = x₁

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

F_3_IN_GAA₁(s_1₁(X)) -> F_3_IN_GAA₁(X)
F_3_IN_GAA₁(s_1₁(X)) -> IF_F_3_IN_1_GAA₁(f_3_in_gaa₁(X))

The TRS R consists of the following rules:

f_3_in_gaa₁(s_1₁(X)) -> if_f_3_in_1_gaa₁(f_3_in_gaa₁(X))
if_f_3_in_2_gaa₁(f_3_out_gaa₁(Z)) -> f_3_out_gaa₁(Z)

The set Q consists of the following terms:

f_3_in_gaa₁(x0)
if_f_3_in_1_gaa₁(x0)
if_f_3_in_2_gaa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {F_3_IN_GAA₁, IF_F_3_IN_1_GAA₁}.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ UsableRulesProof

                        ↳ QDP

                          ↳ RuleRemovalProof

Q DP problem:
The TRS P consists of the following rules:

F_3_IN_GAA₁(s_1₁(X)) -> F_3_IN_GAA₁(X)
F_3_IN_GAA₁(s_1₁(X)) -> IF_F_3_IN_1_GAA₁(f_3_in_gaa₁(X))

The TRS R consists of the following rules:

f_3_in_gaa₁(s_1₁(X)) -> if_f_3_in_1_gaa₁(f_3_in_gaa₁(X))

The set Q consists of the following terms:

f_3_in_gaa₁(x0)
if_f_3_in_1_gaa₁(x0)
if_f_3_in_2_gaa₁(x0)

F_3_IN_GAA₁(s_1₁(X)) -> F_3_IN_GAA₁(X)
F_3_IN_GAA₁(s_1₁(X)) -> IF_F_3_IN_1_GAA₁(f_3_in_gaa₁(X))

Strictly oriented rules of the TRS R:

f_3_in_gaa₁(s_1₁(X)) -> if_f_3_in_1_gaa₁(f_3_in_gaa₁(X))

Used ordering: POLO with Polynomial interpretation:

POL(if_f_3_in_1_gaa₁(x₁)) = 1 + x₁
POL(F_3_IN_GAA₁(x₁)) = x₁
POL(s_1₁(x₁)) = 2 + x₁
POL(IF_F_3_IN_1_GAA₁(x₁)) = x₁
POL(f_3_in_gaa₁(x₁)) = 1 + x₁

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ UsableRulesProof

                        ↳ QDP

                          ↳ RuleRemovalProof

                            ↳ QDP

                              ↳ PisEmptyProof

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

f_3_in_gaa₁(x0)
if_f_3_in_1_gaa₁(x0)
if_f_3_in_2_gaa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are empty set.
The TRS P is empty. Hence, there is no (P,Q,R) chain.